Inference at * 1 1 
Iof proof for Lemma decidable implies better:



1. P : 
2. Q : x:P.
3. Dec(P)
4. P  Dec(Q)
  Dec(P  Q) 

latex

 by Unfold `decidable` 0 THEN D (-2)  

latex

 1: 

 1: 3. P
 1: 4. P  Dec(Q)
 1:   (P  Q)  ((P  Q))
 2: 

 2: 3. P
 2: 4. P  Dec(Q)
 2:   (P  Q)  ((P  Q))
 .

Definitions

Dec(P), P  Q